\begin{tabbing}
h{-}ordered(${\it es}$;$e$.$P$($e$);$H$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $P$($e$)\} .\+
\\[0ex]($e$ $\in$ $H$($e$) $\in$ es{-}E(${\it es}$))
\\[0ex]\& (\=$\forall$${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $P$($e$)\} .\+
\\[0ex](es{-}causle(${\it es}$;$e$;${\it e'}$) $\Rightarrow$ ($e$ $\in$ $H$(${\it e'}$) $\in$ es{-}E(${\it es}$)))
\\[0ex]\& (($e$ $\in$ $H$(${\it e'}$) $\in$ es{-}E(${\it es}$)) $\vee$ (${\it e'}$ $\in$ $H$($e$) $\in$ es{-}E(${\it es}$)))
\\[0ex]\& (($e$ $\in$ $H$(${\it e'}$) $\in$ es{-}E(${\it es}$)) $\Rightarrow$ (${\it e'}$ $\in$ $H$($e$) $\in$ es{-}E(${\it es}$)) $\Rightarrow$ ($e$ = ${\it e'}$ $\in$ es{-}E(${\it es}$)))
\\[0ex]\& (($e$ $\in$ $H$(${\it e'}$) $\in$ es{-}E(${\it es}$)) $\Rightarrow$ $H$($e$) $\leq$ $H$(${\it e'}$) $\in$ es{-}E(${\it es}$) List))
\-\-
\end{tabbing}